| 1: | terms(N) | → cons(recip(sqr(N)),n__terms(n__s(N))) | |
| 2: | sqr(0) | → 0 | |
| 3: | sqr(s(X)) | → s(add(sqr(X),dbl(X))) | |
| 4: | dbl(0) | → 0 | |
| 5: | dbl(s(X)) | → s(s(dbl(X))) | |
| 6: | add(0,X) | → X | |
| 7: | add(s(X),Y) | → s(add(X,Y)) | |
| 8: | first(0,X) | → nil | |
| 9: | first(s(X),cons(Y,Z)) | → cons(Y,n__first(X,activate(Z))) | |
| 10: | terms(X) | → n__terms(X) | |
| 11: | s(X) | → n__s(X) | |
| 12: | first(X1,X2) | → n__first(X1,X2) | |
| 13: | activate(n__terms(X)) | → terms(activate(X)) | |
| 14: | activate(n__s(X)) | → s(activate(X)) | |
| 15: | activate(n__first(X1,X2)) | → first(activate(X1),activate(X2)) | |
| 16: | activate(X) | → X | |
| 17: | TERMS(N) | → SQR(N) | |
| 18: | SQR(s(X)) | → S(add(sqr(X),dbl(X))) | |
| 19: | SQR(s(X)) | → ADD(sqr(X),dbl(X)) | |
| 20: | SQR(s(X)) | → SQR(X) | |
| 21: | SQR(s(X)) | → DBL(X) | |
| 22: | DBL(s(X)) | → S(s(dbl(X))) | |
| 23: | DBL(s(X)) | → S(dbl(X)) | |
| 24: | DBL(s(X)) | → DBL(X) | |
| 25: | ADD(s(X),Y) | → S(add(X,Y)) | |
| 26: | ADD(s(X),Y) | → ADD(X,Y) | |
| 27: | FIRST(s(X),cons(Y,Z)) | → ACTIVATE(Z) | |
| 28: | ACTIVATE(n__terms(X)) | → TERMS(activate(X)) | |
| 29: | ACTIVATE(n__terms(X)) | → ACTIVATE(X) | |
| 30: | ACTIVATE(n__s(X)) | → S(activate(X)) | |
| 31: | ACTIVATE(n__s(X)) | → ACTIVATE(X) | |
| 32: | ACTIVATE(n__first(X1,X2)) | → FIRST(activate(X1),activate(X2)) | |
| 33: | ACTIVATE(n__first(X1,X2)) | → ACTIVATE(X1) | |
| 34: | ACTIVATE(n__first(X1,X2)) | → ACTIVATE(X2) | |